n, m:, f:(nm). Inj(n; m; f)  nm 

latex

Definitions	i>j, S  T, l[i], A & B, P  Q, Dec(P), i  j < k, x. t(x), ||as||, sum(f(x) | x < k), P & Q, x:A. B(x), t  T, x:A. B(x), , {i..j}, Inj(A; B; f), P  Q, False, A, AB
Lemmas	inject wf, int seg wf, nat wf, finite-partition, sum bound, le wf, length wf1, decidable le, select wf, not wf